Make hoare_seq_ext and hoare_vcg_seqE wp rules #748
Conversation
corlewis
added
cleanup
proof engineering
A couple of the changes were because of |
| apply (wp whenE_throwError_wp hoare_vcg_imp_lift hoare_drop_imps | ||
| | strengthen aag_Control_owns_strg | ||
| | simp add: o_def del: hoare_True_E_R)+ | ||
| apply (wpsimp wp: weak_if_wp) |
There was a problem hiding this comment.
could you say something about what weak_if_wp is or when to use it? (not in the commits, but I've either not heard of it or completely forgot)
There was a problem hiding this comment.
⟦ ⦃P⦄ f ⦃Q⦄; ⦃P'⦄ f ⦃Q'⦄ ⟧ ⟹ ⦃P and P'⦄ f ⦃λr. if C r then Q r else Q' r⦄
In my mind it's for when there's an if in the postcondition where you don't need to know the if condition and don't want to lift it across the function for whatever reason.
From memory, my cases in this PR were generally if conditions on the return value that would have been painful to lift, and where the two branches were either roughly the same or one was a form of True. As an alternative I probably could have used the simplifier to handle the if, but this approach with weak_if_wp was the one I found first.
There was a problem hiding this comment.
That's awesome, I hope I won't forget it. It feels better than exciting combination of if_apply_def2 and hoare_drop_imps, and should work in more cases. It's interesting that this isn't achieved with a wp <some_rule>, but I guess it does need to shuffle the order.
We want them as wp rules instead of wp_split rules so that they are used with the correct priority and in combination with wp_comb rules when necessary. This also adds new validE_R and validE_E variants, along with rules for when bind appears inside a validE term. Signed-off-by: Corey Lewis <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
This is no longer necessary now that the nondet monad setup already makes it a wp rule. Signed-off-by: Corey Lewis <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
corlewis
force-pushed
the
hoare_seq_ext_wp
branch
from
034bf83
to
bf45b3d
Compare
hoare_seq_extwas previously made awprule in the middle ofainvs, which was surprising and could lead to different behaviour depending on which session a proof was inside of. This change makes it awprule in the baseMonadssetup, along with improving consistency by adding similar rules forvalidEand its variants.